\begin{tabbing} Raframe{-}loc($x_{1}$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $x_{1}$ of \+ \\[0ex]Rnone =$>$ $\cdot$ \\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.$\cdot$ \\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ $\cdot$ \\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ $\cdot$ \\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ $\cdot$ \\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ $\cdot$ \\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ $\cdot$ \\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$p$,$P$)=$>$ $\cdot$ \\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ ${\it loc}$ \\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ $\cdot$ \\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ $\cdot$ \- \end{tabbing}